\begin{figure}[!t]
\begin{smaller}
\def\codesmaller{\smaller}
\begin{description}
  \item[Ownership nesting]
    The first owner parameter of type~\hT must be inside
        any other owner parameter in~\hT.

  \item[Field access]
    Field access~\code{o.f} is legal
        iff~\underline{$\Ofn{\code{f}}=\This \Rightarrow \code{o}={\this}$}.

  \item[Field assignment]
    Field assignment~\code{o.f=\ldots} is legal iff
        (i)~$\Ifn{\code{o}} \st \Raw$, and
        (ii)~$\big(\Ifn{\code{o}} = \Raw \Rightarrow (\code{o}=\this\text{~or~}\Ofn{\code{o}} = \This)\big)$, and
        (iii)~field access~\code{o.f} is legal.

  \item[Method invocation]
    Consider method~\code{T$_0$ m(T$_1$,\ldots,T$_n$)}.
    The invocation~\code{o.m(\ldots)} is legal
        iff
        (i)~\underline{$\Ofn{\code{T}_i}=\This \Rightarrow \code{o}={\this}$} for~$i=0,\ldots,n$, and
        (ii)~$\Ifn{\code{m}} = \Raw$ implies field assignment part (ii).

    %Typing method \emph{parameters} is the same as field \emph{assignment} part (ii)--(iii),
    %    and typing the \emph{return type} is the same as field \emph{access}.

  \item[cJ's method guard]
    (i)~An invocation~\code{o.m(\ldots)} is legal if the type of~\code{o} satisfies the guard of~\code{m}.
    (ii)~When typing method~\hm, the bound of type variables that appear in the guard
        changes to their bound in the guard.
    (iii)~The guard of an overriding method is
        equivalent or weaker than that of the overridden method.

  \item[Inner classes]
    An inner class reuses the owner parameter of the outer class.
    However, it has a distinct immutability parameter.

  \item[Invariant]
    The programmer marks each type parameter as invariant or covariant.
%    The todo{Use of ``the'' here is very confusing here and many other
%      places, such as in the ``Generic wildcards'' rule, since there can be
%      multiple immutability parameters.  Should this be ``an immutability
%      parameter''?  Or is there a specific one you mean?  The same goes for
%    ``the owner parameter'' (e.g., in ``Generic wildcards'' rule).}
    An immutability parameter is always covariant,
     whereas an owner parameter is always invariant.

    A type parameter must be invariant if it is used in
        a superclass that contains \Mutable,
        a field that contains \Mutable but is not \this-owned,
        or in the position of another invariant type parameter.


  \item[Same-class subtype relation]
    Let $\hC\hgn{\hX_1,\ldots,\hX_n}$ be a class.
    Type $\hS=\hC\hgn{\hS_1,\ldots,\hS_n}$ is
        \emph{a subtype of} $\hT=\hC\hgn{\hT_1,\ldots,\hT_n}$,
        written as $\hS\st\hT$,
        iff
        ($\hS=\hT$) or
        \Big((all immutability parameters $\hT_j$ are either \ReadOnly{} or \Immut{}),
        and for~$i=1,\ldots,n$, \big($\hS_i=\hT_i$ or ($\hS_i \st \hT_i$ and $\hX_i$ is covariant in \hC)\big)\Big).
% See Invariant rule: todo{``covariant in \hC'' needs to be defined.}

  \item[Erased signature]
    If method~\code{m}$'$ overrides a readonly/immutable method~\code{m}, %and \mbox{$\Immut \st \Ifn{\code{m}}$},
        then the erased signatures of~\code{m}$'$ and~\code{m}, excluding invariant
        type parameters, must be identical.
    (The \emph{erased signature} of a method is obtained by replacing type parameters
        with their bounds.)

  \item[Object creation]
    A constructor cannot have any \this-owned arguments.
    Furthermore, \code{new SomeClass\hgn{X,\ldots}(\ldots)} is legal iff
        the constructor's guard \code{<I extends Y>?}
        satisfies:
        $\code{Y}=\Mutable$ and $\code{X}=\Mutable$, or $\code{Y}=\Raw$.

  \item[Generic Wildcards]
    OIGJ prohibits using a generic wildcard (\code{?})
        in the position of the immutability parameter.
    For the owner parameter,
        OIGJ prohibits using a wildcard in a field or in a method return type,
        but permits it
        for stack variables and method parameters.

  \item[\Raw parameter]
    \code{Raw} can only be used after the {\code{extends}} keyword.
    It cannot be used in the position of
        a generic parameter.

  \item[Fresh owners]
    A \emph{fresh owner} is a method owner parameter
        that is not used in the method signature.
    It is a descendant in the ownership tree of all other owners in scope.

  \item[Static context]
    \This{} cannot be used in a static context (static methods or \rlap{fields).}
\end{description}
\end{smaller}
\def\codesmaller{\small}
\caption{All the OIGJ typing rules (beyond those of Java), in English.  Also see \Ref{Section}{formal} for
  a formalization. Underlined sentences show similarities among the rules.
  }
\label{Figure:oigj-typing-rules}
\end{figure}

% LocalWords:  cJ's readonly SomeClass Wildcards wildcards
